Viewing 0 current events matching “OS design” by Date.

Sort By: Date Event Name, Location , Default
No events were found.

Viewing 1 past event matching “OS design” by Date.

Sort By: Date Event Name, Location , Default
Tuesday
Oct 16, 2012
Galois Tech Talk: Towards a Formally Verified Component Platform
Galois, Inc

Presented by Matthew Fernandez.

In safety- and security-critical environments software failures that are acceptable in other contexts may have expensive or even life-threatening consequences. Formal verification has the potential to provide high assurance for this software, but is regarded as being prohibitively expensive. Although significant advances have been made in this area, verification of larger systems still remains impractical. Component-based development has the potential to lower the cost of system-wide verification, bringing correctness proofs of these large scale systems within reach. This talk will discuss my work that aims to provide a component-based development environment for building systems with high assurance requirements. By providing a formal model of the platform with proven correctness properties that hold at the level of an abstract model right down to the implementation, I hope to reduce the cost of full system verification by allowing reasoning about system components in isolation.

Website